Step of Proof: add_functionality_wrt_le
12,41
postcript
pdf
Inference at
*
1
1
I
of proof for Lemma
add
functionality
wrt
le
:
1.
i1
:
2.
i2
:
3.
j2
:
4.
i2
j2
j1
:
. (
i1
j1
)
((
i1
+
i2
)
(
j1
+
j2
))
latex
by (RA (IntInd 1))
latex
1
:
1:
1.
i2
:
1:
2.
j2
:
1:
3.
i2
j2
1:
4.
i1
:
1:
5.
i1
< 0
1:
6.
j1
:
. ((
i1
+1)
j1
)
((
i1
+1+
i2
)
(
j1
+
j2
))
1:
7.
j1
:
1:
8.
i1
j1
1:
(
i1
+
i2
)
(
j1
+
j2
)
2
:
2:
1.
i2
:
2:
2.
j2
:
2:
3.
i2
j2
2:
4.
j1
:
2:
5. 0
j1
2:
(0+
i2
)
(
j1
+
j2
)
3
:
3:
1.
i2
:
3:
2.
j2
:
3:
3.
i2
j2
3:
4.
i1
:
3:
5. 0 <
i1
3:
6.
j1
:
. ((
i1
- 1)
j1
)
(((
i1
- 1)+
i2
)
(
j1
+
j2
))
3:
7.
j1
:
3:
8.
i1
j1
3:
(
i1
+
i2
)
(
j1
+
j2
)
.
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
Lemmas
le
wf
origin